$\forall$${\it es}$:ES, $A$, $B$:Type, ${\it Ia}$:AbsInterface($A$), $f$:($A$$\rightarrow$$B$), $Q$:(E(${\it Ia}$)$\rightarrow$E(${\it Ia}$)$\rightarrow\mathbb{P}$).
\\[0ex]$\lambda$$e$.$e$ glues ${\it Ia}$:$Q$ $--\lambda$$e$.$f$(${\it Ia}$($e$))$\rightarrow$ $f$'${\it Ia}$:$Q$